Covered languages in this unit will all be computable/decidable which means we will be working in intuitionistic logic.

Terminology

A judgement is a claim that something holds some property. In order to prove it is true, we must provide some evidence using rules, once that is done, it is an evidenced judgement.

Rules have names, and consist of some (possibly none) premises which are placed on the top, and a conclusion which goes on the bottom. The name goes to the right of these. %%🖋 Edit in Excalidraw%% A rule with no premises, is an axiom.

---

Our Rules

%%🖋 Edit in Excalidraw%%

Proofs

Proof that two is a natural number

%%🖋 Edit in Excalidraw%%

Proof that two is even

%%🖋 Edit in Excalidraw%%

Derivable & Admissible Rules

An admissible rule is any rule that is not necessary, i.e. a rule where if we have a derivation of the premise, we know that we can construct a derivation of the conclusion.

A rule is derivable if we can use a derivation of its premise (what goes on top) as a building block in deriving its conclusion.

Example of a Derivable Rule

%%🖋 Edit in Excalidraw%% Not every admissible rule is derivable, but if a rule is derivable it is admissible.

This rule is admissible but not derivable, because anything we could assemble with it, we could do with the existing $S$ rule: %%🖋 Edit in Excalidraw%%

Induction

%%🖋 Edit in Excalidraw%%

Cards

Q: What is the relationship between derivable and admissible rules? A: Derivable => admissible, but not the reverse

Q: What is the structure of a rule? A: